Skip to content

Refactor mlk_polymat_permute_bitrev_to_custom#1336

Open
mkannwischer wants to merge 1 commit intomainfrom
refactor-polymat-permute
Open

Refactor mlk_polymat_permute_bitrev_to_custom#1336
mkannwischer wants to merge 1 commit intomainfrom
refactor-polymat-permute

Conversation

@mkannwischer
Copy link
Copy Markdown
Contributor

@mkannwischer mkannwischer commented Dec 3, 2025 •
edited
Loading

This commit refactors mlk_polymat_permute_bitrev_to_custom to not require the helper function mlk_polyvec_permute_bitrev_to_custom. The function was only needed due CBMC limitations.

@mkannwischer mkannwischer force-pushed the refactor-polymat-permute branch from 18ed177 to 28046a2 Compare December 3, 2025 09:18
@mkannwischer
Copy link
Copy Markdown
Contributor Author

mkannwischer commented Dec 3, 2025 •
edited
Loading

This proves fine in a couple of seconds for MLKEM_K=3, but spins forever for MLKEM_K=2 and MLKEM_K=4:

$ tests cbmc -p polymat_permute_bitrev_to_custom_native --k 3

For your convenience, the output of this run will be symbolically linked to  /Users/matthiaskannwischer/git/native/mlkem-native/proofs/cbmc/output/latest/html/index.html 

Configuring CBMC proofs: 1 / 1
[16/16] mlk_polymat_permute_bitrev_to_custom_native: generating report                                                                                                                                                                                                                                                                                                  
Report was rendered at file:///Users/matthiaskannwischer/git/native/mlkem-native/proofs/cbmc/output/latest/html/index.html
## Summary of CBMC proof results

| Status  | Count |
|---------|-------|
| Success | 1     |

| Proof                                       | Status  | Duration (in s) |
|---------------------------------------------|---------|-----------------|
| mlk_polymat_permute_bitrev_to_custom_native | Success | 6               |


WARNING:root:$GITHUB_STEP_SUMMARY not set, not writing summary file
All good!
Matthiass-MacBook-Pro:mlkem-native matthiaskannwischer$ tests cbmc -p polymat_permute_bitrev_to_custom_native --k 2

For your convenience, the output of this run will be symbolically linked to  /Users/matthiaskannwischer/git/native/mlkem-native/proofs/cbmc/output/latest/html/index.html 

Configuring CBMC proofs: 1 / 1
[14/16] mlk_polymat_permute_bitrev_to_custom_native: printing safety properties

Makes no sense to me.
@rod-chapman, any ideas?

@rod-chapman
Copy link
Copy Markdown
Contributor

rod-chapman commented Dec 3, 2025

Since we introduced struct wrappers around mlk_polyvec and mlk_polymat, the latter is now a struct that contains a K-element array of structs, each of which contains a single K-element array of mlk_poly.

This new code is trying to treat that as a single-dimensional array of K*K mlk_poly's by the look of it. That's bound to cause serious complications for CBMC.

Try a nested loop, so the code structure matches the data structure.

@rod-chapman rod-chapman force-pushed the refactor-polymat-permute branch from cc0d751 to 782e470 Compare December 18, 2025 11:04
@hanno-becker
Copy link
Copy Markdown
Contributor

hanno-becker commented Jan 2, 2026

@mkannwischer Can you comment on state/plans for this?

@mkannwischer
Copy link
Copy Markdown
Contributor Author

mkannwischer commented Jan 6, 2026

@mkannwischer Can you comment on state/plans for this?

See pq-code-package/mldsa-native#770 - we are waiting for diffblue/cbmc#8705 to be merged.

@willieyz, could you rebase this PR and also include the experimental branch of CBMC so we can confirm that the proofs pass with that version.

@willieyz
Copy link
Copy Markdown
Contributor

willieyz commented Jan 6, 2026

@mkannwischer Can you comment on state/plans for this?

See pq-code-package/mldsa-native#770 - we are waiting for diffblue/cbmc#8705 to be merged.

@willieyz, could you rebase this PR and also include the experimental branch of CBMC so we can confirm that the proofs pass with that version.

Yes, I can do it.

@willieyz willieyz force-pushed the refactor-polymat-permute branch 5 times, most recently from 1745ecc to d5b04b1 Compare January 7, 2026 01:56
@hanno-becker
Copy link
Copy Markdown
Contributor

hanno-becker commented Mar 19, 2026

This seems no longer relevant; closing. @mkannwischer reopen if you disagree and foresee time to work on this.

@mkannwischer
Copy link
Copy Markdown
Contributor Author

mkannwischer commented Mar 19, 2026 •
edited
Loading

This seems no longer relevant; closing. @mkannwischer reopen if you disagree and foresee time to work on this.

Why is this no longer relevant? I still want to do this refactoring as soon as the CBMC fix has been merged.

@mkannwischer mkannwischer reopened this Mar 19, 2026
@rod-chapman
Copy link
Copy Markdown
Contributor

rod-chapman commented Mar 19, 2026

Agree. We will return to this when we get a new release of CBMC. The helper function could be removed if and when CBMC can handle a nested loop efficiently.

@rod-chapman rod-chapman force-pushed the refactor-polymat-permute branch 2 times, most recently from fe13eb9 to 4afccb7 Compare April 20, 2026 14:26
@willieyz @rod-chapman
Refactor mlk_polymat_permute_bitrev_to_custom
9f86f86 
This commit refactors mlk_polymat_permute_bitrev_to_custom to not require the
helper function mlk_polyvec_permute_bitrev_to_custom.
The function was only needed due CBMC limitations.

The code structure now mimics the data structure to make proof tractable.
Also updates Makefile for this proof in line with the similar function
in mldsa-native.

Signed-off-by: Matthias J. Kannwischer <matthias@kannwischer.eu>
Signed-off-by: Rod Chapman <rodchap@amazon.com>
Signed-off-by: willieyz <willie.zhao@chelpis.com>

Re-format with clang-format and add decreases contract

Signed-off-by: Rod Chapman <rodchap@amazon.com>
@rod-chapman rod-chapman force-pushed the refactor-polymat-permute branch from 4afccb7 to 9f86f86 Compare April 20, 2026 14:27
@rod-chapman rod-chapman self-assigned this Apr 20, 2026
@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Apr 20, 2026

CBMC Results (ML-KEM-1024)

Full Results (190 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 1364s 1296s +5.2%
mlk_indcpa_enc ✅ 169s 146s +16%
mlk_indcpa_keypair_derand ✅ 146s 134s +9%
mlk_rej_uniform_c ✅ 113s 144s -22%
mlk_polymat_permute_bitrev_to_custom_native ✅ 87s - new
mlk_polyvec_basemul_acc_montgomery_cached_c ✅ 73s 84s -13%
mlk_ntt_layer ✅ 41s 37s +11%
polyvec_basemul_acc_montgomery_cached_native ✅ 36s 37s -3%
mlk_poly_rej_uniform ✅ 33s 32s +3%
poly_ntt_native ✅ 28s 31s -10%
mlk_keccak_squeezeblocks_x4 ✅ 27s 25s +8%
mlk_poly_reduce_native ✅ 24s 22s +9%
keccakf1600x4_permute_native_x4 ✅ 19s 19s +0%
mlk_fqmul ✅ 19s 17s +12%
mlk_poly_decompress_d11_native ✅ 15s 14s +7%
mlk_poly_decompress_d5_native ✅ 14s 16s -12%
mlk_poly_frommsg ✅ 10s 11s -9%
mlk_keccak_squeeze_once ✅ 9s 7s +29%
mlk_keccak_squeezeblocks ✅ 9s 10s -10%
mlk_poly_frombytes_native ✅ 9s 12s -25%
mlk_polyvec_add ✅ 9s 12s -25%
kem_dec ✅ 8s 7s +14%
mlk_indcpa_dec ✅ 8s 10s -20%
mlk_poly_ntt ✅ 7s 8s -12%
poly_frombytes_native_x86_64 ✅ 7s 5s +40%
mlk_check_pct ✅ 6s 2s +200%
mlk_gen_matrix ✅ 6s 5s +20%
mlk_keccak_absorb_once_x4 ✅ 6s 7s -14%
mlk_ntt_butterfly_block ✅ 6s 9s -33%
mlk_poly_rej_uniform_x4 ✅ 6s 6s +0%
poly_decompress_d5_native_x86_64 ✅ 6s 6s +0%
mlk_invntt_layer ✅ 5s 6s -17%
mlk_keccak_absorb_once ✅ 5s 4s +25%
mlk_keccakf1600_permute_c ✅ 5s 6s -17%
mlk_poly_compress_d11_c ✅ 5s 5s +0%
mlk_poly_compress_d5 ✅ 5s 4s +25%
mlk_poly_decompress_d4_c ✅ 5s 3s +67%
mlk_polyvec_frombytes ✅ 5s 2s +150%
mlk_scalar_compress_d11 ✅ 5s 2s +150%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 ✅ 5s 3s +67%
rej_uniform_native_x86_64 ✅ 5s 5s +0%
keccak_f1600_x4_native_avx2 ✅ 4s 3s +33%
kem_enc ✅ 4s 3s +33%
mlk_ct_get_optblocker_u32 ✅ 4s 1s +300%
mlk_gen_matrix_serial ✅ 4s 3s +33%
mlk_keypair_getnoise_eta1 ✅ 4s 4s +0%
mlk_montgomery_reduce ✅ 4s 2s +100%
mlk_poly_compress_d11 ✅ 4s 2s +100%
mlk_poly_compress_du ✅ 4s 3s +33%
mlk_poly_compress_dv ✅ 4s 1s +300%
mlk_poly_decompress_d4_native ✅ 4s 2s +100%
mlk_poly_mulcache_compute_c ✅ 4s 2s +100%
mlk_poly_mulcache_compute_native ✅ 4s 3s +33%
mlk_poly_reduce ✅ 4s 1s +300%
mlk_poly_tobytes_native ✅ 4s 2s +100%
mlk_polyvec_tomont ✅ 4s 3s +33%
poly_decompress_d11_native_x86_64 ✅ 4s 3s +33%
poly_decompress_d4_native_x86_64 ✅ 4s 1s +300%
rej_uniform_native ✅ 4s 1s +300%
keccakf1600_permute_native ✅ 3s 2s +50%
kem_check_pk ✅ 3s 3s +0%
kem_enc_derand ✅ 3s 2s +50%
kem_keypair ✅ 3s 4s -25%
kem_keypair_derand ✅ 3s 1s +200%
mlk_ct_cmov_zero ✅ 3s 2s +50%
mlk_ct_get_optblocker_i32 ✅ 3s 2s +50%
mlk_ct_sel_int16 ✅ 3s 5s -40%
mlk_enc_getnoise_eta1_eta2 ✅ 3s 4s -25%
mlk_keccakf1600_extract_bytes (big endian) ✅ 3s 4s -25%
mlk_keccakf1600x4_extract_bytes_c ✅ 3s 1s +200%
mlk_keccakf1600x4_permute ✅ 3s 1s +200%
mlk_poly_cbd_eta1 ✅ 3s 3s +0%
mlk_poly_compress_d10 ✅ 3s 3s +0%
mlk_poly_compress_d4_c ✅ 3s 2s +50%
mlk_poly_compress_d5_native ✅ 3s 1s +200%
mlk_poly_decompress_d11 ✅ 3s 2s +50%
mlk_poly_decompress_d5_c ✅ 3s 3s +0%
mlk_poly_decompress_du ✅ 3s 3s +0%
mlk_poly_decompress_dv ✅ 3s 2s +50%
mlk_poly_frombytes_c ✅ 3s 1s +200%
mlk_poly_getnoise_eta1122_4x ✅ 3s 2s +50%
mlk_poly_getnoise_eta1_4x_native ✅ 3s 3s +0%
mlk_poly_getnoise_eta2 ✅ 3s 4s -25%
mlk_poly_invntt_tomont ✅ 3s 2s +50%
mlk_poly_invntt_tomont_c ✅ 3s 2s +50%
mlk_poly_mulcache_compute ✅ 3s 2s +50%
mlk_poly_ntt_c ✅ 3s 3s +0%
mlk_poly_tobytes ✅ 3s 1s +200%
mlk_poly_tomont ✅ 3s 2s +50%
mlk_poly_tomsg ✅ 3s 3s +0%
mlk_polyvec_basemul_acc_montgomery_cached ✅ 3s 2s +50%
mlk_polyvec_compress_du ✅ 3s 2s +50%
mlk_polyvec_invntt_tomont ✅ 3s 3s +0%
mlk_polyvec_ntt ✅ 3s 3s +0%
mlk_polyvec_tobytes ✅ 3s 3s +0%
mlk_scalar_compress_d1 ✅ 3s 3s +0%
mlk_scalar_compress_d10 ✅ 3s 2s +50%
mlk_scalar_compress_d5 ✅ 3s 5s -40%
mlk_sha3_256 ✅ 3s 2s +50%
mlk_sha3_512 ✅ 3s 2s +50%
mlk_shake128x4_squeezeblocks ✅ 3s 1s +200%
ntt_native_aarch64 ✅ 3s 3s +0%
nttunpack_native_x86_64 ✅ 3s 3s +0%
poly_decompress_d10_native_x86_64 ✅ 3s 2s +50%
poly_invntt_tomont_native ✅ 3s 3s +0%
poly_mulcache_compute_native_x86_64 ✅ 3s 2s +50%
poly_reduce_native_aarch64 ✅ 3s 3s +0%
poly_reduce_native_x86_64 ✅ 3s 1s +200%
poly_tomont_native_x86_64 ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 ✅ 3s 3s +0%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 ✅ 3s 2s +50%
rej_uniform_native_aarch64 ✅ 3s 2s +50%
intt_native_x86_64 ✅ 2s 5s -60%
keccak_f1600_x1_native_aarch64 ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v84a ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 2s 2s +0%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 2s 2s +0%
keccakf1600x4_xor_bytes_native ✅ 2s 2s +0%
mlk_barrett_reduce ✅ 2s 4s -50%
mlk_ct_cmask_neg_i16 ✅ 2s 3s -33%
mlk_ct_cmask_nonzero_u16 ✅ 2s 3s -33%
mlk_ct_memcmp ✅ 2s 5s -60%
mlk_ct_sel_uint8 ✅ 2s 3s -33%
mlk_keccakf1600_extract_bytes ✅ 2s 4s -50%
mlk_keccakf1600_permute ✅ 2s 2s +0%
mlk_keccakf1600_xor_bytes ✅ 2s 1s +100%
mlk_keccakf1600_xor_bytes (big endian) ✅ 2s 3s -33%
mlk_keccakf1600x4_extract_bytes ✅ 2s 1s +100%
mlk_keccakf1600x4_xor_bytes_c ✅ 2s 3s -33%
mlk_matvec_mul ✅ 2s 4s -50%
mlk_poly_cbd_eta2 ✅ 2s 2s +0%
mlk_poly_compress_d10_native ✅ 2s 2s +0%
mlk_poly_compress_d11_native ✅ 2s 3s -33%
mlk_poly_compress_d5_c ✅ 2s 4s -50%
mlk_poly_decompress_d10_c ✅ 2s 3s -33%
mlk_poly_decompress_d10_native ✅ 2s 3s -33%
mlk_poly_decompress_d4 ✅ 2s 3s -33%
mlk_poly_decompress_d5 ✅ 2s 2s +0%
mlk_poly_frombytes ✅ 2s 2s +0%
mlk_poly_getnoise_eta1_4x ✅ 2s 4s -50%
mlk_poly_reduce_c ✅ 2s 5s -60%
mlk_poly_sub ✅ 2s 3s -33%
mlk_poly_tobytes_c ✅ 2s 3s -33%
mlk_poly_tomont_c ✅ 2s 2s +0%
mlk_poly_tomont_native ✅ 2s 2s +0%
mlk_polyvec_mulcache_compute ✅ 2s 2s +0%
mlk_rej_uniform ✅ 2s 2s +0%
mlk_scalar_compress_d4 ✅ 2s 4s -50%
mlk_scalar_decompress_d10 ✅ 2s 3s -33%
mlk_scalar_decompress_d5 ✅ 2s 3s -33%
mlk_shake128_squeezeblocks ✅ 2s 1s +100%
mlk_shake256x4 ✅ 2s 4s -50%
mlk_value_barrier_i32 ✅ 2s 3s -33%
ntt_native_x86_64 ✅ 2s 2s +0%
poly_compress_d10_native_x86_64 ✅ 2s 2s +0%
poly_compress_d4_native_x86_64 ✅ 2s 1s +100%
poly_compress_d5_native_x86_64 ✅ 2s 2s +0%
poly_tomont_native_aarch64 ✅ 2s 3s -33%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 ✅ 2s 3s -33%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 ✅ 2s 1s +100%
intt_native_aarch64 ✅ 1s 2s -50%
keccak_f1600_x1_native_aarch64_v84a ✅ 1s 3s -67%
keccakf1600x4_extract_bytes_native ✅ 1s 3s -67%
kem_check_sk ✅ 1s 2s -50%
mlk_ct_cmask_nonzero_u8 ✅ 1s 1s +0%
mlk_ct_get_optblocker_u8 ✅ 1s 2s -50%
mlk_keccakf1600x4_xor_bytes ✅ 1s 2s -50%
mlk_poly_add ✅ 1s 5s -80%
mlk_poly_compress_d10_c ✅ 1s 3s -67%
mlk_poly_compress_d4 ✅ 1s 1s +0%
mlk_poly_compress_d4_native ✅ 1s 2s -50%
mlk_poly_decompress_d10 ✅ 1s 2s -50%
mlk_poly_decompress_d11_c ✅ 1s 3s -67%
mlk_polymat_permute_bitrev_to_custom ✅ 1s 6s -83%
mlk_polyvec_decompress_du ✅ 1s 4s -75%
mlk_polyvec_reduce ✅ 1s 4s -75%
mlk_scalar_decompress_d11 ✅ 1s 3s -67%
mlk_scalar_decompress_d4 ✅ 1s 2s -50%
mlk_scalar_signed_to_unsigned_q ✅ 1s 1s +0%
mlk_shake128_absorb_once ✅ 1s 2s -50%
mlk_shake128x4_absorb_once ✅ 1s 1s +0%
mlk_shake256 ✅ 1s 2s -50%
mlk_value_barrier_u32 ✅ 1s 2s -50%
mlk_value_barrier_u8 ✅ 1s 2s -50%
poly_compress_d11_native_x86_64 ✅ 1s 2s -50%
poly_getnoise_eta1122_4x_native ✅ 1s 2s -50%
poly_mulcache_compute_native_aarch64 ✅ 1s 3s -67%
poly_tobytes_native_aarch64 ✅ 1s 2s -50%
poly_tobytes_native_x86_64 ✅ 1s 3s -67%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 ✅ 1s 3s -67%
sys_check_capability ✅ 1s 1s +0%

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Apr 20, 2026

CBMC Results (ML-KEM-512)

Full Results (190 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 1301s 1256s +3.6%
mlk_indcpa_keypair_derand ✅ 211s 243s -13%
mlk_indcpa_enc ✅ 162s 160s +1%
mlk_rej_uniform_c ✅ 119s 110s +8%
mlk_polyvec_basemul_acc_montgomery_cached_c ✅ 49s 51s -4%
mlk_polymat_permute_bitrev_to_custom_native ✅ 48s - new
mlk_ntt_layer ✅ 29s 28s +4%
mlk_poly_rej_uniform ✅ 29s 28s +4%
poly_ntt_native ✅ 26s 23s +13%
mlk_keccak_squeezeblocks_x4 ✅ 22s 24s -8%
keccakf1600x4_permute_native_x4 ✅ 18s 18s +0%
mlk_indcpa_dec ✅ 18s 13s +38%
mlk_poly_reduce_native ✅ 18s 20s -10%
mlk_fqmul ✅ 16s 16s +0%
mlk_poly_decompress_d10_native ✅ 15s 12s +25%
mlk_poly_decompress_d4_native ✅ 13s 13s +0%
mlk_poly_frommsg ✅ 9s 8s +12%
mlk_polyvec_add ✅ 9s 10s -10%
mlk_keccak_squeezeblocks ✅ 8s 8s +0%
mlk_poly_frombytes_native ✅ 8s 6s +33%
mlk_keccak_absorb_once_x4 ✅ 7s 5s +40%
mlk_keccak_squeeze_once ✅ 7s 7s +0%
mlk_poly_rej_uniform_x4 ✅ 7s 7s +0%
mlk_invntt_layer ✅ 6s 7s -14%
mlk_ntt_butterfly_block ✅ 6s 9s -33%
mlk_poly_ntt ✅ 6s 7s -14%
mlk_scalar_decompress_d4 ✅ 6s 1s +500%
poly_decompress_d4_native_x86_64 ✅ 6s 5s +20%
polyvec_basemul_acc_montgomery_cached_native ✅ 6s 6s +0%
mlk_keccakf1600_permute_c ✅ 5s 6s -17%
mlk_poly_cbd_eta2 ✅ 5s 5s +0%
mlk_poly_compress_d10_c ✅ 5s 4s +25%
mlk_poly_tomont_native ✅ 5s 3s +67%
poly_reduce_native_x86_64 ✅ 5s 3s +67%
poly_tomont_native_aarch64 ✅ 5s 1s +400%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 ✅ 5s 2s +150%
intt_native_aarch64 ✅ 4s 4s +0%
keccak_f1600_x4_native_aarch64_v84a ✅ 4s 3s +33%
keccakf1600_permute_native ✅ 4s 3s +33%
kem_check_pk ✅ 4s 4s +0%
kem_dec ✅ 4s 5s -20%
kem_enc ✅ 4s 2s +100%
mlk_keccakf1600x4_xor_bytes ✅ 4s 4s +0%
mlk_poly_compress_d10 ✅ 4s 3s +33%
mlk_poly_compress_d11_native ✅ 4s 2s +100%
mlk_poly_compress_d4_c ✅ 4s 2s +100%
mlk_poly_decompress_d11_native ✅ 4s 4s +0%
mlk_poly_getnoise_eta1_4x ✅ 4s 2s +100%
mlk_poly_reduce_c ✅ 4s 1s +300%
mlk_polyvec_basemul_acc_montgomery_cached ✅ 4s 2s +100%
mlk_polyvec_compress_du ✅ 4s 3s +33%
mlk_scalar_compress_d5 ✅ 4s 3s +33%
mlk_value_barrier_i32 ✅ 4s 4s +0%
poly_decompress_d10_native_x86_64 ✅ 4s 4s +0%
poly_frombytes_native_x86_64 ✅ 4s 5s -20%
poly_getnoise_eta1122_4x_native ✅ 4s 2s +100%
poly_mulcache_compute_native_x86_64 ✅ 4s 2s +100%
poly_tobytes_native_aarch64 ✅ 4s 3s +33%
rej_uniform_native ✅ 4s 2s +100%
keccak_f1600_x1_native_aarch64_v84a ✅ 3s 2s +50%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 3s 2s +50%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 3s 3s +0%
keccakf1600x4_extract_bytes_native ✅ 3s 4s -25%
mlk_check_pct ✅ 3s 5s -40%
mlk_ct_cmask_neg_i16 ✅ 3s 2s +50%
mlk_ct_cmov_zero ✅ 3s 2s +50%
mlk_ct_get_optblocker_i32 ✅ 3s 2s +50%
mlk_ct_get_optblocker_u32 ✅ 3s 1s +200%
mlk_ct_sel_uint8 ✅ 3s 2s +50%
mlk_enc_getnoise_eta1_eta2 ✅ 3s 3s +0%
mlk_gen_matrix_serial ✅ 3s 3s +0%
mlk_keccak_absorb_once ✅ 3s 4s -25%
mlk_keccakf1600_extract_bytes (big endian) ✅ 3s 2s +50%
mlk_keccakf1600x4_xor_bytes_c ✅ 3s 2s +50%
mlk_poly_add ✅ 3s 2s +50%
mlk_poly_compress_d4 ✅ 3s 2s +50%
mlk_poly_compress_d4_native ✅ 3s 3s +0%
mlk_poly_decompress_d4 ✅ 3s 1s +200%
mlk_poly_decompress_d4_c ✅ 3s 3s +0%
mlk_poly_decompress_d5_c ✅ 3s 2s +50%
mlk_poly_decompress_d5_native ✅ 3s 3s +0%
mlk_poly_decompress_du ✅ 3s 4s -25%
mlk_poly_frombytes_c ✅ 3s 1s +200%
mlk_poly_getnoise_eta1122_4x ✅ 3s 2s +50%
mlk_poly_mulcache_compute_native ✅ 3s 5s -40%
mlk_poly_tobytes_c ✅ 3s 2s +50%
mlk_poly_tomsg ✅ 3s 4s -25%
mlk_polyvec_mulcache_compute ✅ 3s 3s +0%
mlk_polyvec_ntt ✅ 3s 4s -25%
mlk_polyvec_tobytes ✅ 3s 2s +50%
mlk_polyvec_tomont ✅ 3s 1s +200%
mlk_scalar_compress_d1 ✅ 3s 2s +50%
mlk_shake128x4_absorb_once ✅ 3s 3s +0%
mlk_shake256 ✅ 3s 1s +200%
mlk_shake256x4 ✅ 3s 4s -25%
nttunpack_native_x86_64 ✅ 3s 2s +50%
poly_compress_d10_native_x86_64 ✅ 3s 2s +50%
poly_compress_d11_native_x86_64 ✅ 3s 1s +200%
poly_compress_d5_native_x86_64 ✅ 3s 1s +200%
poly_decompress_d5_native_x86_64 ✅ 3s 1s +200%
poly_mulcache_compute_native_aarch64 ✅ 3s 4s -25%
poly_reduce_native_aarch64 ✅ 3s 1s +200%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 ✅ 3s 3s +0%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 ✅ 3s 3s +0%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 ✅ 3s 3s +0%
sys_check_capability ✅ 3s 1s +200%
intt_native_x86_64 ✅ 2s 3s -33%
keccak_f1600_x1_native_aarch64 ✅ 2s 1s +100%
kem_check_sk ✅ 2s 2s +0%
kem_enc_derand ✅ 2s 2s +0%
kem_keypair ✅ 2s 1s +100%
kem_keypair_derand ✅ 2s 2s +0%
mlk_ct_cmask_nonzero_u16 ✅ 2s 3s -33%
mlk_ct_get_optblocker_u8 ✅ 2s 2s +0%
mlk_ct_memcmp ✅ 2s 1s +100%
mlk_ct_sel_int16 ✅ 2s 1s +100%
mlk_keccakf1600_xor_bytes (big endian) ✅ 2s 2s +0%
mlk_keccakf1600x4_extract_bytes ✅ 2s 1s +100%
mlk_keccakf1600x4_extract_bytes_c ✅ 2s 3s -33%
mlk_keypair_getnoise_eta1 ✅ 2s 3s -33%
mlk_matvec_mul ✅ 2s 2s +0%
mlk_poly_cbd_eta1 ✅ 2s 3s -33%
mlk_poly_compress_d10_native ✅ 2s 3s -33%
mlk_poly_compress_d11_c ✅ 2s 3s -33%
mlk_poly_compress_d5 ✅ 2s 3s -33%
mlk_poly_compress_d5_c ✅ 2s 2s +0%
mlk_poly_compress_d5_native ✅ 2s 2s +0%
mlk_poly_compress_dv ✅ 2s 2s +0%
mlk_poly_decompress_d10 ✅ 2s 3s -33%
mlk_poly_decompress_d10_c ✅ 2s 3s -33%
mlk_poly_decompress_d11 ✅ 2s 3s -33%
mlk_poly_decompress_d11_c ✅ 2s 1s +100%
mlk_poly_decompress_d5 ✅ 2s 2s +0%
mlk_poly_getnoise_eta2 ✅ 2s 3s -33%
mlk_poly_invntt_tomont ✅ 2s 4s -50%
mlk_poly_invntt_tomont_c ✅ 2s 4s -50%
mlk_poly_mulcache_compute ✅ 2s 2s +0%
mlk_poly_ntt_c ✅ 2s 2s +0%
mlk_poly_reduce ✅ 2s 2s +0%
mlk_poly_sub ✅ 2s 2s +0%
mlk_poly_tobytes ✅ 2s 4s -50%
mlk_poly_tomont ✅ 2s 3s -33%
mlk_poly_tomont_c ✅ 2s 3s -33%
mlk_polymat_permute_bitrev_to_custom ✅ 2s 2s +0%
mlk_polyvec_decompress_du ✅ 2s 3s -33%
mlk_polyvec_frombytes ✅ 2s 2s +0%
mlk_polyvec_invntt_tomont ✅ 2s 2s +0%
mlk_polyvec_reduce ✅ 2s 1s +100%
mlk_rej_uniform ✅ 2s 2s +0%
mlk_scalar_compress_d10 ✅ 2s 1s +100%
mlk_scalar_compress_d11 ✅ 2s 1s +100%
mlk_scalar_compress_d4 ✅ 2s 3s -33%
mlk_scalar_decompress_d10 ✅ 2s 4s -50%
mlk_scalar_decompress_d5 ✅ 2s 2s +0%
mlk_scalar_signed_to_unsigned_q ✅ 2s 3s -33%
mlk_sha3_512 ✅ 2s 3s -33%
mlk_shake128_absorb_once ✅ 2s 2s +0%
mlk_shake128_squeezeblocks ✅ 2s 1s +100%
mlk_value_barrier_u8 ✅ 2s 4s -50%
ntt_native_x86_64 ✅ 2s 2s +0%
poly_compress_d4_native_x86_64 ✅ 2s 3s -33%
poly_decompress_d11_native_x86_64 ✅ 2s 3s -33%
poly_invntt_tomont_native ✅ 2s 3s -33%
poly_tobytes_native_x86_64 ✅ 2s 4s -50%
poly_tomont_native_x86_64 ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 ✅ 2s 3s -33%
rej_uniform_native_aarch64 ✅ 2s 4s -50%
rej_uniform_native_x86_64 ✅ 2s 2s +0%
keccak_f1600_x4_native_avx2 ✅ 1s 2s -50%
keccakf1600x4_xor_bytes_native ✅ 1s 1s +0%
mlk_barrett_reduce ✅ 1s 3s -67%
mlk_ct_cmask_nonzero_u8 ✅ 1s 3s -67%
mlk_gen_matrix ✅ 1s 4s -75%
mlk_keccakf1600_extract_bytes ✅ 1s 4s -75%
mlk_keccakf1600_permute ✅ 1s 2s -50%
mlk_keccakf1600_xor_bytes ✅ 1s 2s -50%
mlk_keccakf1600x4_permute ✅ 1s 2s -50%
mlk_montgomery_reduce ✅ 1s 2s -50%
mlk_poly_compress_d11 ✅ 1s 1s +0%
mlk_poly_compress_du ✅ 1s 1s +0%
mlk_poly_decompress_dv ✅ 1s 2s -50%
mlk_poly_frombytes ✅ 1s 3s -67%
mlk_poly_getnoise_eta1_4x_native ✅ 1s 2s -50%
mlk_poly_mulcache_compute_c ✅ 1s 1s +0%
mlk_poly_tobytes_native ✅ 1s 1s +0%
mlk_scalar_decompress_d11 ✅ 1s 2s -50%
mlk_sha3_256 ✅ 1s 2s -50%
mlk_shake128x4_squeezeblocks ✅ 1s 3s -67%
mlk_value_barrier_u32 ✅ 1s 2s -50%
ntt_native_aarch64 ✅ 1s 2s -50%

@oqs-bot
Copy link
Copy Markdown
Contributor

oqs-bot commented Apr 20, 2026

CBMC Results (ML-KEM-768)

Full Results (190 proofs)
Proof Status Current Previous Change
**TOTAL** ✅ 1275s 1399s -8.9%
mlk_indcpa_enc ✅ 166s 196s -15%
mlk_indcpa_keypair_derand ✅ 161s 221s -27%
mlk_rej_uniform_c ✅ 133s 166s -20%
mlk_polyvec_basemul_acc_montgomery_cached_c ✅ 47s 49s -4%
mlk_ntt_layer ✅ 33s 41s -20%
mlk_poly_rej_uniform ✅ 32s 34s -6%
mlk_polymat_permute_bitrev_to_custom_native ✅ 31s - new
mlk_keccak_squeezeblocks_x4 ✅ 25s 28s -11%
poly_ntt_native ✅ 25s 32s -22%
mlk_poly_reduce_native ✅ 20s 22s -9%
keccakf1600x4_permute_native_x4 ✅ 17s 18s -6%
mlk_fqmul ✅ 17s 18s -6%
polyvec_basemul_acc_montgomery_cached_native ✅ 17s 19s -11%
mlk_poly_decompress_d10_native ✅ 15s 20s -25%
mlk_poly_decompress_d4_native ✅ 14s 17s -18%
mlk_indcpa_dec ✅ 13s 14s -7%
mlk_poly_frombytes_native ✅ 10s 10s +0%
mlk_keccak_squeezeblocks ✅ 9s 10s -10%
mlk_poly_frommsg ✅ 9s 12s -25%
mlk_polyvec_add ✅ 9s 9s +0%
mlk_keccak_squeeze_once ✅ 8s 8s +0%
mlk_ntt_butterfly_block ✅ 8s 9s -11%
mlk_poly_decompress_du ✅ 7s 3s +133%
mlk_poly_ntt ✅ 7s 9s -22%
mlk_poly_compress_d10_c ✅ 6s 3s +100%
mlk_poly_compress_d4 ✅ 6s 3s +100%
kem_dec ✅ 5s 4s +25%
mlk_ct_cmov_zero ✅ 5s 2s +150%
mlk_gen_matrix ✅ 5s 3s +67%
mlk_invntt_layer ✅ 5s 5s +0%
mlk_keccak_absorb_once ✅ 5s 3s +67%
mlk_keccak_absorb_once_x4 ✅ 5s 7s -29%
mlk_keccakf1600_permute_c ✅ 5s 6s -17%
mlk_poly_decompress_d5 ✅ 5s 2s +150%
mlk_poly_reduce ✅ 5s 2s +150%
mlk_poly_rej_uniform_x4 ✅ 5s 9s -44%
mlk_scalar_decompress_d4 ✅ 5s 1s +400%
nttunpack_native_x86_64 ✅ 5s 1s +400%
keccak_f1600_x4_native_aarch64_v8a_v84a_scalar_hybrid ✅ 4s 4s +0%
kem_check_pk ✅ 4s 4s +0%
kem_enc_derand ✅ 4s 2s +100%
mlk_keccakf1600_extract_bytes (big endian) ✅ 4s 3s +33%
mlk_poly_compress_du ✅ 4s 4s +0%
mlk_poly_decompress_d11 ✅ 4s 2s +100%
mlk_poly_frombytes ✅ 4s 2s +100%
mlk_poly_frombytes_c ✅ 4s 1s +300%
mlk_poly_getnoise_eta1122_4x ✅ 4s 2s +100%
mlk_poly_tomsg ✅ 4s 3s +33%
mlk_polymat_permute_bitrev_to_custom ✅ 4s 6s -33%
mlk_scalar_decompress_d5 ✅ 4s 2s +100%
mlk_sha3_512 ✅ 4s 3s +33%
mlk_shake256x4 ✅ 4s 3s +33%
mlk_value_barrier_u8 ✅ 4s 4s +0%
ntt_native_aarch64 ✅ 4s 2s +100%
poly_compress_d10_native_x86_64 ✅ 4s 1s +300%
poly_decompress_d10_native_x86_64 ✅ 4s 6s -33%
poly_decompress_d4_native_x86_64 ✅ 4s 7s -43%
poly_tomont_native_aarch64 ✅ 4s 2s +100%
polyvec_basemul_acc_montgomery_cached_k3_native_aarch64 ✅ 4s 4s +0%
rej_uniform_native ✅ 4s 2s +100%
keccak_f1600_x1_native_aarch64_v84a ✅ 3s 3s +0%
keccakf1600x4_extract_bytes_native ✅ 3s 2s +50%
kem_keypair ✅ 3s 4s -25%
kem_keypair_derand ✅ 3s 4s -25%
mlk_check_pct ✅ 3s 4s -25%
mlk_ct_cmask_nonzero_u16 ✅ 3s 2s +50%
mlk_ct_sel_int16 ✅ 3s 5s -40%
mlk_gen_matrix_serial ✅ 3s 2s +50%
mlk_keccakf1600x4_xor_bytes ✅ 3s 1s +200%
mlk_keypair_getnoise_eta1 ✅ 3s 1s +200%
mlk_poly_compress_d10 ✅ 3s 2s +50%
mlk_poly_compress_d11_c ✅ 3s 2s +50%
mlk_poly_compress_d11_native ✅ 3s 3s +0%
mlk_poly_compress_d5 ✅ 3s 2s +50%
mlk_poly_compress_dv ✅ 3s 2s +50%
mlk_poly_decompress_d10_c ✅ 3s 1s +200%
mlk_poly_decompress_d4 ✅ 3s 2s +50%
mlk_poly_decompress_d4_c ✅ 3s 2s +50%
mlk_poly_decompress_d5_native ✅ 3s 4s -25%
mlk_poly_getnoise_eta1_4x ✅ 3s 2s +50%
mlk_poly_invntt_tomont ✅ 3s 2s +50%
mlk_poly_invntt_tomont_c ✅ 3s 1s +200%
mlk_poly_mulcache_compute_c ✅ 3s 3s +0%
mlk_poly_ntt_c ✅ 3s 6s -50%
mlk_poly_sub ✅ 3s 1s +200%
mlk_poly_tomont_native ✅ 3s 3s +0%
mlk_polyvec_basemul_acc_montgomery_cached ✅ 3s 1s +200%
mlk_polyvec_decompress_du ✅ 3s 2s +50%
mlk_polyvec_invntt_tomont ✅ 3s 2s +50%
mlk_polyvec_mulcache_compute ✅ 3s 3s +0%
mlk_polyvec_reduce ✅ 3s 2s +50%
mlk_polyvec_tomont ✅ 3s 2s +50%
mlk_scalar_compress_d10 ✅ 3s 1s +200%
mlk_scalar_compress_d5 ✅ 3s 2s +50%
mlk_scalar_signed_to_unsigned_q ✅ 3s 2s +50%
poly_compress_d11_native_x86_64 ✅ 3s 1s +200%
poly_compress_d4_native_x86_64 ✅ 3s 2s +50%
poly_frombytes_native_x86_64 ✅ 3s 8s -62%
poly_mulcache_compute_native_aarch64 ✅ 3s 1s +200%
poly_mulcache_compute_native_x86_64 ✅ 3s 2s +50%
poly_reduce_native_x86_64 ✅ 3s 5s -40%
poly_tobytes_native_aarch64 ✅ 3s 2s +50%
poly_tobytes_native_x86_64 ✅ 3s 3s +0%
polyvec_basemul_acc_montgomery_cached_k2_native_aarch64 ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_k2_native_x86_64 ✅ 3s 2s +50%
polyvec_basemul_acc_montgomery_cached_k3_native_x86_64 ✅ 3s 4s -25%
polyvec_basemul_acc_montgomery_cached_k4_native_x86_64 ✅ 3s 1s +200%
rej_uniform_native_x86_64 ✅ 3s 3s +0%
intt_native_aarch64 ✅ 2s 1s +100%
intt_native_x86_64 ✅ 2s 3s -33%
keccak_f1600_x4_native_avx2 ✅ 2s 2s +0%
kem_check_sk ✅ 2s 1s +100%
mlk_barrett_reduce ✅ 2s 3s -33%
mlk_ct_cmask_neg_i16 ✅ 2s 2s +0%
mlk_ct_cmask_nonzero_u8 ✅ 2s 3s -33%
mlk_ct_get_optblocker_i32 ✅ 2s 2s +0%
mlk_ct_get_optblocker_u32 ✅ 2s 3s -33%
mlk_ct_get_optblocker_u8 ✅ 2s 1s +100%
mlk_ct_sel_uint8 ✅ 2s 2s +0%
mlk_enc_getnoise_eta1_eta2 ✅ 2s 1s +100%
mlk_keccakf1600_extract_bytes ✅ 2s 3s -33%
mlk_keccakf1600_xor_bytes ✅ 2s 2s +0%
mlk_keccakf1600_xor_bytes (big endian) ✅ 2s 3s -33%
mlk_keccakf1600x4_extract_bytes ✅ 2s 5s -60%
mlk_keccakf1600x4_extract_bytes_c ✅ 2s 2s +0%
mlk_keccakf1600x4_permute ✅ 2s 2s +0%
mlk_matvec_mul ✅ 2s 3s -33%
mlk_montgomery_reduce ✅ 2s 1s +100%
mlk_poly_add ✅ 2s 3s -33%
mlk_poly_cbd_eta1 ✅ 2s 3s -33%
mlk_poly_cbd_eta2 ✅ 2s 3s -33%
mlk_poly_compress_d10_native ✅ 2s 2s +0%
mlk_poly_compress_d4_c ✅ 2s 2s +0%
mlk_poly_compress_d4_native ✅ 2s 2s +0%
mlk_poly_compress_d5_native ✅ 2s 4s -50%
mlk_poly_decompress_d11_c ✅ 2s 2s +0%
mlk_poly_decompress_d11_native ✅ 2s 1s +100%
mlk_poly_decompress_dv ✅ 2s 3s -33%
mlk_poly_getnoise_eta1_4x_native ✅ 2s 1s +100%
mlk_poly_mulcache_compute ✅ 2s 4s -50%
mlk_poly_reduce_c ✅ 2s 4s -50%
mlk_poly_tobytes ✅ 2s 3s -33%
mlk_poly_tomont ✅ 2s 3s -33%
mlk_poly_tomont_c ✅ 2s 2s +0%
mlk_polyvec_compress_du ✅ 2s 3s -33%
mlk_polyvec_frombytes ✅ 2s 3s -33%
mlk_polyvec_ntt ✅ 2s 2s +0%
mlk_polyvec_tobytes ✅ 2s 3s -33%
mlk_rej_uniform ✅ 2s 2s +0%
mlk_scalar_compress_d11 ✅ 2s 2s +0%
mlk_scalar_compress_d4 ✅ 2s 1s +100%
mlk_scalar_decompress_d10 ✅ 2s 4s -50%
mlk_scalar_decompress_d11 ✅ 2s 3s -33%
mlk_sha3_256 ✅ 2s 2s +0%
mlk_shake128_squeezeblocks ✅ 2s 2s +0%
mlk_shake128x4_absorb_once ✅ 2s 2s +0%
mlk_value_barrier_i32 ✅ 2s 2s +0%
mlk_value_barrier_u32 ✅ 2s 1s +100%
ntt_native_x86_64 ✅ 2s 3s -33%
poly_compress_d5_native_x86_64 ✅ 2s 3s -33%
poly_decompress_d11_native_x86_64 ✅ 2s 3s -33%
poly_getnoise_eta1122_4x_native ✅ 2s 2s +0%
poly_reduce_native_aarch64 ✅ 2s 2s +0%
polyvec_basemul_acc_montgomery_cached_k4_native_aarch64 ✅ 2s 2s +0%
keccak_f1600_x1_native_aarch64 ✅ 1s 2s -50%
keccak_f1600_x4_native_aarch64_v84a ✅ 1s 3s -67%
keccak_f1600_x4_native_aarch64_v8a_scalar_hybrid ✅ 1s 2s -50%
keccakf1600_permute_native ✅ 1s 3s -67%
keccakf1600x4_xor_bytes_native ✅ 1s 2s -50%
kem_enc ✅ 1s 2s -50%
mlk_ct_memcmp ✅ 1s 2s -50%
mlk_keccakf1600_permute ✅ 1s 1s +0%
mlk_keccakf1600x4_xor_bytes_c ✅ 1s 2s -50%
mlk_poly_compress_d11 ✅ 1s 2s -50%
mlk_poly_compress_d5_c ✅ 1s 4s -75%
mlk_poly_decompress_d10 ✅ 1s 3s -67%
mlk_poly_decompress_d5_c ✅ 1s 3s -67%
mlk_poly_getnoise_eta2 ✅ 1s 2s -50%
mlk_poly_mulcache_compute_native ✅ 1s 2s -50%
mlk_poly_tobytes_c ✅ 1s 1s +0%
mlk_poly_tobytes_native ✅ 1s 3s -67%
mlk_scalar_compress_d1 ✅ 1s 1s +0%
mlk_shake128_absorb_once ✅ 1s 3s -67%
mlk_shake128x4_squeezeblocks ✅ 1s 1s +0%
mlk_shake256 ✅ 1s 4s -75%
poly_decompress_d5_native_x86_64 ✅ 1s 2s -50%
poly_invntt_tomont_native ✅ 1s 4s -75%
poly_tomont_native_x86_64 ✅ 1s 2s -50%
rej_uniform_native_aarch64 ✅ 1s 1s +0%
sys_check_capability ✅ 1s 1s +0%

@rod-chapman rod-chapman marked this pull request as ready for review April 20, 2026 17:47
@rod-chapman rod-chapman requested a review from a team as a code owner April 20, 2026 17:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

@rod-chapman rod-chapman

@hanno-becker hanno-becker

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

CBMC: Refactor mlk_polymat_permute_bitrev_to_custom and prove monolithically

5 participants

@mkannwischer @rod-chapman @hanno-becker @willieyz @oqs-bot